Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(g,app(h,app(g,x)))  → app(g,x)
2:    app(g,app(g,x))  → app(g,app(h,app(g,x)))
3:    app(h,app(h,x))  → app(h,app(app(f,app(h,x)),x))
There are 5 dependency pairs:
4:    APP(g,app(g,x))  → APP(g,app(h,app(g,x)))
5:    APP(g,app(g,x))  → APP(h,app(g,x))
6:    APP(h,app(h,x))  → APP(h,app(app(f,app(h,x)),x))
7:    APP(h,app(h,x))  → APP(app(f,app(h,x)),x)
8:    APP(h,app(h,x))  → APP(f,app(h,x))
The approximated dependency graph contains 2 SCCs: {6} and {4}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.04 seconds)   ---  May 4, 2006